Nuprl Lemma : fpf-all-empty
0,22
postcript
pdf
A
:Type,
eq
,
P
:Top.
y
dom().
w
=(
y
)
P
(
y
,
w
)
True
latex
Definitions
Top
,
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
x
dom(
f
)
,
b
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
(
s1
,
s2
)
,
False
,
t
T
,
True
Lemmas
true
wf
,
false
wf
,
top
wf
origin
A:Type, eq, P:Top. y
dom(). w=(y) 
P(y,w) 
True A:Type, eq, P:Top. ydom(). w=(y) P(y,w) True xdom(f). v=f(x) P(x;v) dom(f)
b Q Qx:A. B(x) Q T